/*************************************************************************
	> File Name: maxTomin.c
	> Author:
	> Mail:
	> Created Time: 2017年02月04日 星期六 14时07分14秒
 ************************************************************************/

#include<stdio.h>
#include <stdlib.h>
#include<klee/klee.h>
#include "klee_change_macros.h"
int main(int argc, char* argv[]){
    int a,b,d;
    a=atoi(argv[1]);
    b=atoi(argv[2]);
    char *as="old version", *bs="new version";
    char * ss=as;
    if(a<4)
    {
        FILE *ff=fopen("file","w+");
          fprintf(ff,"%s\n",ss);
          fclose(ff);
    }
    else
        printf("%s\n", ss);

    return 0;
}
